E:Type, pred?:(E(?E)), info:(E((:Id  Id) + (:(:IdLnk  E)  Id))), V:(IdIdType),
M:(IdLnkIdType), T:(IdIdType), init:(i:IdEState((T(i)))),
Trans:(i:Idk:Kndkindcase(k; a.(V(i,a)); l,t.(M(l,t)))EState((T(i)))EState((T(i)))),
Choose:(i,a:Id(x:IdT(i,x))(?(V(i,a)))), Send:(i:Idk:Kndkindcase(k;
Choose:(i,a:Id(x:IdT(i,x))(?(V(i,a)))), Send:(i:Idk:Kndkindcase(a.(V(i,a));
Choose:(i,a:Id(x:IdT(i,x))(?(V(i,a)))), Send:(i:Idk:Kndkindcase(l,t.(M(l,t)))
Choose:(i,a:Id(x:IdT(i,x))(?(V(i,a)))), Send:((x:IdT(i,x))(Msg(M) List)),
val:(e:Ekindcase(kind(e); a.(V(loc(e),a)); l,t.(M(l,t)))), time:(Erationals).
(e:E. ((first(e)))  (loc(pred(e)) = loc(e)  Id))
 SWellFounded(pred!(e;e'))
 (val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time)  prop{i:l}) 

latex

Definitions

b, x:A. B(x), P  Q, sender(e), t  T, state_when(e), EState(T), rationals, x:AB(x), guard(T), sq_type(T), Knd, prop{i:l}, sqequal(s; t), False, islocal(k), rcv(l,tg), tag(k), lnk(k), A, b, , P  Q, P  Q, Unit, kindcase(k; a.f(a); l,t.g(l;t)), Type, A  B, , {x:A| B(x)} , , act(k), <a, b>, Msg(M), True, isrcv(k), locl(a), ecase1(e;info;i.f(i);l,e'.g(l;e')), rcv?(e), kind(e), subtype(S; T), inr x , #$n, x.A(x), isl(x), x,y. t(x;y), x. t(x), type List, loc(e), void, isect(A; x.B(x)), top, suptype(S; T), pred(e), first(e), pred!(e;e'), SWellFounded(R(x;y)), (x  l), outl(x), A c B, x:A. B(x), val-axiom(E;V;M;info;pred?;init;Trans;Choose;Send;val;time), f(a), Id, IdLnk, x:A  B(x), left + right, s = t

Lemmas

islocal wf, outl wf, isrcv wf, l member wf, strongwellfounded wf, pred! wf, first wf, pred wf, top wf, rationals wf, kind wf, loc wf, Msg wf, nat wf, kindcase wf, EState wf, Id wf, unit wf, isl wf, int inc rationals, IdLnk wf, false wf, true wf, actof wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, bool wf, bnot wf, not wf, assert wf, subtype rel self, lnk wf, tagof wf, isrcv-implies, Knd wf, Knd sq, state when wf, sender wf